COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDVAR u v w x y z ε NATNUM
C00004 ENDMK
C⊗;
DECLARE INDVAR u v w x y z ε NATNUM;
DECLARE OPCONST suc pred(NATNUM)=NATNUM;
DECLARE OPCONST +(NATNUM,NATNUM)=NATNUM [R←450,L←455];
DECLARE OPCONST *(NATNUM,NATNUM)=NATNUM [R←550,L←555];
DECLARE PREDPAR P 1;

AXIOM 	S:
	SUCC:	∀x.¬(0=suc(x));
	ONEONE:	∀x y.(suc(x)=suc(y)⊃x=y);
	PLUS:	∀x.x+0=0
		∀x y.x+suc(y)=suc(x+y);
	TIMES:  ∀x.x*0=0
		∀x y.x*suc(y)=(x*y)+y;

	INDUCT:	P(0) ∧ ∀x.(P(x)⊃P(suc(x))) ⊃ ∀x.P(x); ;;

REPRESENT {NATNUM} AS NATNUMREP;
ATTACH suc  ↔ (LAMBDA (X) (ADD1 X));
ATTACH pred ↔ (LAMBDA (X) (COND ((GREATERP X 0)(SUB1 X)) (T 0)));
ATTACH +    ↔ (LAMBDA (X Y) (PLUS X Y));
ATTACH *    ↔ (LAMBDA (X Y) (TIMES X Y));

DECLARE OPCONST fact(NATNUM)=NATNUM;
AXIOM FACT: ∀x.fact(x)=IF x=0 THEN 1 ELSE x*fact(pred(x)) ;;